-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

-- Usage:
--
--  Set up the environment
--     setenv LD_LIBRARY_PATH /opt/exp/gnu/lib:$LD_LIBRARY_PATH
--     setenv PATH /home/ggreif/%NoBackup%/Omega1.4.2:$PATH
--
--  Start the omega interpreter by typing
--     omega MonadPrime.omg
--  and run your commands on the prompt
--

import "LangPrelude.prg" 
  (head,tail,lookup,member,fst,snd,map,Monad,maybeM,id,ioM,Row,RCons,RNil,Eq,Equal,listM)

import "Thrist.omg" 
  (Thrist, Nil, Cons, syntax List(l))

-- #################################################

data Monad' :: (* ~> *) ~> * ~> * ~> * where
  Feed :: m b -> Monad' m a b
  Feed' :: b -> Monad' m a b
  Digest :: (t -> m u) -> Monad' m t u
  Digest' :: (t -> u) -> Monad' m t u


t0 = let monad maybeM in [Digest (\5 -> return True), Feed $ Just "2"]l
t1 = [Feed $ putStr "dd", Digest (\ () -> returnIO 3)]l
t2 = let monad maybeM in [Digest (\5 -> return True), Feed' "2"]l
t3 = [Digest' (\5 -> True), Feed' "2"]l

runMP :: Monad m -> m a -> Thrist (Monad' m) a b -> m b
runMP _ mon []l = mon
runMP v _ [Feed m; rest]l = runMP v m rest
runMP (v@Monad return _ _) _ [Feed' m; rest]l = runMP v (return m) rest
runMP (v@Monad _ bind _) mon [Digest f; rest]l = runMP v (bind mon f) rest
runMP (v@Monad return bind _) mon [Digest' f; rest]l = runMP v (bind mon (return . f)) rest

r0 = runMP ioM (returnIO 5) t1


-- fmap' -- ???? does this make sense?
fmap'  :: (m -> n) -> Thrist (Monad' m) a b -> Thrist (Monad' n) a b


{-
-- ##### using "do" syntax for building thrists


data Thrimo :: ((* ~> *) ~> * ~> *) ~> * ~> * where
  Unit :: a -> Thrimo r a
--  Effect :: (r (Thrimo r) a) -> Thrimo r a
  Bind :: (Thrimo r b) -> (b -> Thrimo r a) -> Thrimo r a
  Fail :: String -> Thrimo r a



--thristM :: Monad (Thrist (Monad' m) a)
--thristM = Monad Unit undefined undefined

thristM :: Monad (Thrimo r)
thristM = Monad Unit Bind Fail

mthrist = do { Just a <- Just 5; return a } where monad thristM

--thristize :: Thrimo r -> Thrist (Monad' m) ??????

-}


-- #################################################

-- Thrist extending

extendThrist :: forall (a :: *1) (b :: a ~> a ~> *0) (c :: a) (d :: a) (e :: a) .
		Thrist b c d ->
		b d e ->
		Thrist b c e

extendThrist []l a = [a]l
extendThrist [b; r]l a = [b; extendThrist r a]l


-- Thrist appending

appendThrist :: forall (a :: *1) (b :: a ~> a ~> *0) (c :: a) (d :: a) (e :: a) .
		Thrist b c d ->
		Thrist b d e ->
		Thrist b c e

appendThrist []l a = a
appendThrist [b; r]l a = [b; appendThrist r a]l

-- Thrist flattening

flattenThrist :: forall (l :: *1) (k :: l ~> l ~> *) (a :: l) (b :: l) . Thrist (Thrist k) a b -> Thrist k a b

flattenThrist []l = []l
flattenThrist [a; as]l = appendThrist a $ flattenThrist as

-- Thrist instrumenting

intersperseThrist :: (forall (x :: *). k x x) -> Thrist k a b -> Thrist k a b

intersperseThrist i []l = [i]l
intersperseThrist i [a; as]l = [i, a; intersperseThrist i as]l



-- Pushing down a function into a specific tuple level

p :: Nat ~> * ~> *
{p Z a} = a
{p (S n) a} = (c, {p n a})

nest :: Nat' n -> (a -> b) -> {p n a} -> {p n b}
nest Z f a = f a
nest (S n) f (c, a) = (c, nest n f a)

-- Note: the above works along the right-spine of the structure,
--       we would need another parameter wo walk in left direction too

-- #################################################
-- see Uustalu

data Comonad :: (*0 ~> *0) ~> *0 where
  Comonad :: forall (m :: *0 ~> *0) .
                    ((forall a . m a -> a)) ->
                    ((forall a b . (m a -> b) -> m a -> m b)) ->
                    Comonad m


data Comonad' :: (* ~> *) ~> * ~> * ~> * where
  Peel :: m b -> Comonad' m a b
  Peek :: (m t -> u) -> Comonad' m t u

data Stream a = Then a (Stream a) -- coinductive

streamCM = Comonad counit coextend
           where
             counit (Then a _) = a
             coextend k (af@Then _ as) = Then (k af) (lazy (coextend k as))

ones = Then 1 ones
twos = Then 2 twos

first3 (Then a (Then b (Then c _))) = (a, b + a + c, c)

add3 (Then (a, b, c) _) = a + b + c
fut (Then _ (Then b _)) = b

c1 = [Peel ones, Peek first3]l
c2 = [Peel ones, Peek first3, Peek add3]l
c3 = [Peel ones, Peek first3, Peek add3, Peek fut]l

runCMP :: Comonad c -> c a -> Thrist (Comonad' c) a b -> c b
runCMP _ ca []l = ca
runCMP (com@Comonad _ coextend) ca [Peek comp; rest]l = runCMP com (coextend comp ca) rest
runCMP com _ [Peel new; rest]l = runCMP com new rest

runCMP' :: Comonad c -> c a -> Thrist (Comonad' c) a b -> b
runCMP' (com@Comonad counit _) sta thr = counit (runCMP com sta thr)

-- #################################################
-- see Unimo paper
-- construct monadic law preserving interpreter for
-- Monad'
-- 1) operationally defined Thrist interpreters
-- 2) use Unimo framework to create Omega Monads (Comonads?)


